Simulation-based testing is the most commonly-used method for verifying integrated circuit hardware designs. A software model of the design is prepared, typically using a hardware description language, such as VHDL or Verilog. Different input test patterns are then applied to the model, and the output of the model is inspected for errors. The test patterns may be generated either deterministically or at random. In either case, however, it is impossible to ascertain when enough tests have been performed to adequately cover the entire state space of the design. Therefore, even after lengthy simulation, it is still possible that a design bug may have gone undetected.
Because of the shortcomings of simulation, methods of formal verification, particularly model checking, have been gaining in popularity as tools for use in designing integrated circuits and other complex systems. Such methods are described generally by Clarke et al. in Model Checking (MIT Press, 1999), which is incorporated herein by reference. To perform model checking of the design of a device, a user reads the definition and functional specifications of the device and then, based on this information, writes a set of properties (also known as a specification) that the design is expected to fulfill. The properties are written in a suitable specification language for expressing temporal logic relationships between the inputs and outputs of the device. Such languages are commonly based on Computation Tree Logic (CTL). A hardware model (also known as an implementation) of the design is then tested to ascertain that the model satisfies all of the properties in the set.
After the specification and hardware model have been prepared, the actual model checking is typically carried out automatically using a symbolic model checking program, such as SMV, as described, for example, by McMillan in Symbolic Model Checking (Kluwer Academic Publishers, 1993), which is incorporated herein by reference. A number of practical model checking tools are available, among them RuleBase, developed by IBM Corporation. This tool is described by Beer et al. in RuleBase: an Industry-Oriented Formal Verification Tool, in Proceedings of the Design Automation Conference DAC96 (Las Vegas, Nev., 1996), which is incorporated herein by reference.
Formal verification based on model checking is, in principle, superior to simulation-based testing methods, because model checking covers the entire state space of the target system exhaustively and systematically. Therefore, any violations of the specified properties are certain to be discovered. Existing model checking tools, such as RuleBase, also give the designer a clear exposition of the path through the state space of the model that led to the violation.
Formal verification suffers, however, from the well-known problem of state space explosion. As the modeled system grows larger, the computational resources needed to explore the entire state space grow exponentially. Techniques have been developed for reducing the severity of this problem. Such a technique is described, for example, by Beer et al., in On-the-fly Model Checking of RCTL Formulas, Proceedings of the Tenth International Conference on Computer Aided Verification (CAV 1998), which is incorporated here in by reference. Nevertheless, it appears that simulation testing will still remain part of the design verification tool chest for the foreseeable future.
Although formal verification and simulation are essentially different and separate techniques, some attempts have been made to combine elements of both techniques in a single testing environment. For example, Schlipf et al. describe a methodology and tool for combined formal verification and simulation in Formal Verification Made Easy, IBM Journal of Research and Development 41:4,5 (1997), which is incorporated herein by reference. A state machine formulation is used to represent the specification of the system being verified. If formal verification is not completed within a preset time period (due to state-space explosion), the verification tool switches automatically to random simulation testing.